$\forall$${\it es}$:event\_system\{i:l\}, $x$:Id, $e$:es{-}E(${\it es}$).
\\[0ex]($\neg$($\uparrow$es{-}first(${\it es}$; $e$)))
\\[0ex]$\Rightarrow$ ($\uparrow$es{-}isconst(${\it es}$; loc($e$); $x$))
\\[0ex]$\Rightarrow$ (es{-}after(${\it es}$; $x$; es{-}pred(${\it es}$; $e$)) = es{-}when(${\it es}$; $x$; $e$) $\in$ es{-}vartype(${\it es}$; loc($e$); $x$))